sig VID{}
sig HID{}
sig XID{}
sig EID{}
sig CID{}
sig PID{}
sig Località{}

sig Data{
	giorno: Int,
	mese: Int,
	anno: Int
}{
 	giorno > 0 and mese > 0 and anno > 0
}

sig Ora{
	minuti: Int,
	ora: Int
}{
	minuti >= 0 and ora >= 0
}

abstract sig MezzoDiTrasporto {
	localitàPartenza : one Località,
	localitàArrivo: one Località,
	oraPartenza: one Ora,
	oraArrivo: one Ora,
	dataPartenza: one Data,
	dataArrivo: one Data
}

sig Volo extends MezzoDiTrasporto{
	vid: one VID
}

sig Hotel {
	hid: one HID,
	localitàHotel: one Località
}

sig Escursione {
	xid: one XID,
	dataEx: one Data,
	localitàEx: one Località
}

sig Impiegato{
	eid: one EID,
	pacchettiModificati: set PacchettoViaggio
}

sig UtenteRegistrato{
	cid: one CID,
	prenota: set PacchettoViaggio
}

sig PacchettoViaggio {
	pid: one PID,
   destinazione: one Località,
	voloPartenza: one Volo,
	voloRitorno: one Volo,
	hotel: one Hotel,
	escursioni: set Escursione,
	dataInizio: one Data,
	dataFine: one Data
}



fact differentIDs {
	// 2 pacchetti hanno differenti PID
	no p1, p2: PacchettoViaggio | p1!=p2 and p1.pid = p2.pid
 	// 2 Utenti hanno differenti CID
	no u1,u2: UtenteRegistrato | u1!= u2 and u1.cid = u2.cid
	// 2 impiegati hanno differenti EID
	no e1,e2: Impiegato | e1!=e2 and e1.eid = e2.eid
	// 2 voli hanno differenti VID
	no v1,v2: Volo |v1!=v2 and v1.vid = v2.vid
	// 2 hotel hanno differenti HID
	no h1,h2: Hotel |h1!=h2 and h1.hid = h2.hid
	// 2 escursioni hanno differenti XID
	no x1,x2: Escursione |x1!=x2 and x1.xid = x2.xid
}

fact partenzaArrivoVoloDifferenti{
	no v: Volo | v.localitàPartenza = v.localitàArrivo
}

fact voloPartenzaArrivaDestinazione{
no p: PacchettoViaggio | p.destinazione != voloPartenza.localitàArrivo[p]
}

fact voloRitornoParteDaDestinazione{
no p: PacchettoViaggio | voloRitorno.localitàPartenza[p] != p.destinazione
}

fact noViaggiNelPassato{
all v: Volo | (precedeOra[v.oraPartenza, v.oraArrivo] and stessaData[v.dataPartenza, v.dataArrivo])
	or precedeData[v.dataPartenza, v.dataArrivo]
}

fact voloAndataPrecedeRitorno{
all p: PacchettoViaggio | precedeData[voloPartenza.dataPartenza[p], voloRitorno.dataArrivo[p]]
}

fact durataPacchetto{		
all p: PacchettoViaggio | p.dataInizio = voloPartenza.dataPartenza[p]
all p: PacchettoViaggio | p.dataFine = voloRitorno.dataArrivo[p]
}


fact localitàHotel{
all p: PacchettoViaggio | hotel.localitàHotel[p] = p.destinazione
}

fact coerenzaLocalitàEscursione{
all p: PacchettoViaggio | (all e:p.escursioni | e.localitàEx= p.destinazione)
}

fact coerenzaDataEscursione{
all p: PacchettoViaggio | (all e:p.escursioni | precedeData[e.dataEx, voloRitorno.dataPartenza[p]] 
	and precedeData[voloPartenza.dataArrivo[p], e.dataEx])
}



assert dataEscursionePacchetto{
all p: PacchettoViaggio | ( all e:p.escursioni | precedeData[p.dataInizio, e.dataEx]
and  precedeData[e.dataEx, p.dataFine])
}

assert localitàHotelVolo{
all p: PacchettoViaggio | voloPartenza.localitàArrivo[p] = hotel.localitàHotel[p]
}

assert voloPartenzaRitornoDiversi{
	all p:PacchettoViaggio | p.voloPartenza != p.voloRitorno
 }

assert coerenzaTemporalePacchetto{
	all p:PacchettoViaggio | precedeData[p.dataInizio, p.dataFine]
}



check dataEscursionePacchetto for 3
check localitàHotelVolo for 3
check voloPartenzaRitornoDiversi for 3
check coerenzaTemporalePacchetto for 3



pred precedeData[d1,d2: Data]{
	(d1.anno < d2.anno) or
	(d1.mese < d2.mese and d1.anno <= d2.anno) or
	(d1.giorno <= d2.giorno and d1.mese = d2.mese and d1.anno = d2.anno)	
}

pred stessaData[d1: Data, d2: Data] {
	d1.giorno = d2.giorno and d1.mese = d2.mese and d1.anno = d2.anno
}

pred precedeOra[o1: Ora, o2:Ora]{
	(o1.ora = o2.ora and o1.minuti < o2.minuti) or o1.ora < o2.ora
}

pred show () {}

run show for 2 but exactly 1 PacchettoViaggio
run show for 3 but exactly 1 PacchettoViaggio
